msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
↳ QTRS
↳ DependencyPairsProof
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
MSORT(.(x, y)) → MIN(x, y)
MIN(x, .(y, z)) → MIN(x, z)
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
DEL(x, .(y, z)) → DEL(x, z)
MSORT(.(x, y)) → DEL(min(x, y), .(x, y))
MIN(x, .(y, z)) → MIN(y, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MSORT(.(x, y)) → MIN(x, y)
MIN(x, .(y, z)) → MIN(x, z)
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
DEL(x, .(y, z)) → DEL(x, z)
MSORT(.(x, y)) → DEL(min(x, y), .(x, y))
MIN(x, .(y, z)) → MIN(y, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
DEL(x, .(y, z)) → DEL(x, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DEL(x, .(y, z)) → DEL(x, z)
The value of delta used in the strict ordering is 1.
POL(DEL(x1, x2)) = (4)x_2
POL(.(x1, x2)) = 1/4 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MIN(x, .(y, z)) → MIN(x, z)
MIN(x, .(y, z)) → MIN(y, z)
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MIN(x, .(y, z)) → MIN(x, z)
MIN(x, .(y, z)) → MIN(y, z)
The value of delta used in the strict ordering is 1/16.
POL(MIN(x1, x2)) = (1/4)x_2
POL(.(x1, x2)) = 1/4 + x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MSORT(.(x, y)) → MSORT(del(min(x, y), .(x, y)))
The value of delta used in the strict ordering is 3/64.
POL(if(x1, x2, x3)) = (1/4)x_3
POL(=(x1, x2)) = 0
POL(MSORT(x1)) = (1/4)x_1
POL(.(x1, x2)) = 1/4 + (1/2)x_1
POL(min(x1, x2)) = 0
POL(del(x1, x2)) = (1/4)x_2
POL(nil) = 0
POL(<=(x1, x2)) = 0
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))